TYPES 2003 : types for proofs and programs (Torino, 30 April - 4 May 2003, revised selected papers)Berardi, Stefano; Coppo, Mario; Damiani, Ferruccio et al.Lecture notes in computer science. 2004, issn 0302-9743, isbn 3-540-22164-6, X, 408 p, isbn 3-540-22164-6Conference Proceedings

Program inversion: more than fun!CHEN, W; UDDING, J. T.Science of computer programming. 1990, Vol 15, Num 1, pp 1-13, issn 0167-6423, 13 p.Article

Conception et mise en œuvre d'un système de preuve pour un sous-ensemble de CCS sans transmission de valeurs = Proof system design and implementation for a CCS sub-set without value passingSORIANO, A; VOIRON, J.Rapport de recherche - IMAG. 1985, Num 530, issn 0750-7380, 49 p.Report

LPEQ and DLPEQ: Translators for automated equivalence testing of logic programsJANHUNEN, Tomi; OIKARINEN, Emilia.Lecture notes in computer science. 2004, pp 336-340, issn 0302-9743, isbn 3-540-20721-X, 5 p.Conference Paper

A modular hierarchy of logical frameworksADAMS, Robin.Lecture notes in computer science. 2004, pp 1-16, issn 0302-9743, isbn 3-540-22164-6, 16 p.Conference Paper

Inductive families need not store their indicesBRADY, Edwin; MCBRIDE, Conor; MCKINNA, James et al.Lecture notes in computer science. 2004, pp 115-129, issn 0302-9743, isbn 3-540-22164-6, 15 p.Conference Paper

Applied type system: Extended abstractHONGWEI XI.Lecture notes in computer science. 2004, pp 394-408, issn 0302-9743, isbn 3-540-22164-6, 15 p.Conference Paper

Program extraction from large proof developmentsCRUZ-FILIPE, Luis; SPITTERS, Bas.Lecture notes in computer science. 2003, pp 205-220, issn 0302-9743, isbn 3-540-40664-6, 16 p.Conference Paper

Elimination with a motiveMCBRIDE, Conor.Lecture notes in computer science. 2002, pp 197-216, issn 0302-9743, isbn 3-540-43287-6Conference Paper

Computers and discovery in algebraic graph theoryHANSEN, Pierre; MELOT, Hadrien.Linear algebra and its applications. 2002, Vol 356, pp 211-230, issn 0024-3795Article

Conception d'un langage de haut niveau de représentation de preuves : Récurrence par filtrage de motifs Unification en présence de types inductifs primitifs Synthèse de lemmes d'inversion = Design of a high level language for representing proofs : Recursion and pattern matching Unification in type theories with primitive inductive types Synthesis of inversion lemmasCornes, Cristina; Huet, Gérard.1997, 274 p.Thesis

Preuves et constructions de programmes = Proof and program constructionHUET, G; PAULIN-MOHRING, C.Le Courrier du C.N.R.S. 1993, Num 80, pp 42-43, issn 0153-985XArticle

A generalized iterative construct and its semanticsANSON, E.ACM transactions on programming languages and systems. 1987, Vol 9, Num 4, pp 567-581, issn 0164-0925Article

Total correctness in nonstandard logics of programsSAIN, I; ENGELER, E.Theoretical computer science. 1987, Vol 50, Num 3, pp 285-321, issn 0304-3975Article

The exact security of ECIES in the generic group modelSMART, N. P.Lecture notes in computer science. 2001, pp 73-84, issn 0302-9743, isbn 3-540-43026-1Conference Paper

Un calcul de substitution avec étiquettes = A substitution calculus with labelsGuillaume, Bruno; David, Rene.1999, 96 p.Thesis

Extraction of redundancy-free programs from constructive natural deduction proofsTAKAYAMA, Y.Journal of symbolic computation. 1991, Vol 12, Num 1, pp 29-69, issn 0747-7171Article

Certified SoftwareZHONG SHAO.Communications of the ACM. 2010, Vol 53, Num 12, pp 56-66, issn 0001-0782, 11 p.Article

An interpretation of isabelle/HOL in HOL lightMCLAUGHLIN, Sean.Lecture notes in computer science. 2006, pp 192-204, issn 0302-9743, isbn 3-540-37187-7, 1Vol, 13 p.Conference Paper

Some algebraic structures in lambda-calculus with inductive typesSOLOVIEV, Sergej; CHEMOUIL, David.Lecture notes in computer science. 2004, pp 338-354, issn 0302-9743, isbn 3-540-22164-6, 17 p.Conference Paper

Temporal logic for proof-carrying codeBERNARD, Andrew; LEE, Peter.Lecture notes in computer science. 2002, pp 31-46, issn 0302-9743, isbn 3-540-43931-5, 16 p.Conference Paper

Classifying isomorphic residue classesMEIER, Andreas; POLLET, Martin; SORGE, Volker et al.Lecture notes in computer science. 2001, pp 494-508, issn 0302-9743, isbn 3-540-42959-XConference Paper

Regular expressions revisited : A coinductive approach to streams, automata, and power seriesRUTTEN, J. J. M. M.Lecture notes in computer science. 2000, pp 100-101, issn 0302-9743, isbn 3-540-67727-5Conference Paper

TALP : A tool for the termination analysis of logic programsOHLEBUSCH, E; CLAVES, C; MARCHE, C et al.Lecture notes in computer science. 2000, pp 270-273, issn 0302-9743, isbn 3-540-67778-XConference Paper

Invariant discovery via failed proof attemptsSTARK, J; IRELAND, A.Lecture notes in computer science. 1999, pp 271-288, issn 0302-9743, isbn 3-540-65765-7Conference Paper